Nuprl Definition : append
11,40
postcript
pdf
append(
as
;
bs
) == rec-case(
as
) of [] =>
bs
|
a
::
as'
=>
.cons(
a
; append(
as'
;
bs
))
(recursive)
latex
Definitions
Y
,
x
.
A
(
x
)
,
rec-case(
a
) of [] =>
s
|
x
::
y
=>
z
.
t
(
x
;
y
;
z
)
,
cons(
car
;
cdr
)
,
f
(
a
)
origin
x.A(x), rec-case(a) of [] => s | x::y => z.t(x;y;z), cons(car; cdr), f(a)